{
{ "c::isalnum",
  "#line 1 \"<builtin-library>-isalnum\"\n"
  "\n"
  "inline int isalnum(int c)\n"
  "{ return (c>='a' && c<='z') || (c>='A' && c<='Z') || (c>='0' && c<='9'); }\n"
  "\n"
},
{ "c::isalpha",
  "#line 1 \"<builtin-library>-isalpha\"\n"
  "\n"
  "inline int isalpha(int c)\n"
  "{ return (c>='a' && c<='z') || (c>='A' && c<='Z'); }\n"
  "\n"
},
{ "c::isblank",
  "#line 1 \"<builtin-library>-isblank\"\n"
  "\n"
  "inline int isblank(int c)\n"
  "{ return c==' ' || c=='\\t'; }\n"
  "\n"
},
{ "c::iscntrl",
  "#line 1 \"<builtin-library>-iscntrl\"\n"
  "\n"
  "inline int iscntrl(int c)\n"
  "{ return (c>=0 && c<='\\037') || c=='\\177'; }\n"
  "\n"
},
{ "c::isdigit",
  "#line 1 \"<builtin-library>-isdigit\"\n"
  "\n"
  "inline int isdigit(int c)\n"
  "{ return c>='0' && c<='9'; }\n"
  "\n"
},
{ "c::isgraph",
  "#line 1 \"<builtin-library>-isgraph\"\n"
  "\n"
  "inline int isgraph(int c)\n"
  "{ return c>='!' && c<='~'; }\n"
  "\n"
},
{ "c::islower",
  "#line 1 \"<builtin-library>-islower\"\n"
  "\n"
  "inline int islower(int c)\n"
  "{ return c>='a' && c<='z'; }\n"
  "\n"
},
{ "c::isprint",
  "#line 1 \"<builtin-library>-isprint\"\n"
  "\n"
  "inline int isprint(int c)\n"
  "{ return c>=' ' && c<='~'; }\n"
  "\n"
},
{ "c::ispunct",
  "#line 1 \"<builtin-library>-ispunct\"\n"
  "\n"
  "inline int ispunct(int c)\n"
  "{ return c=='!' ||\n"
  "         c=='\"' ||\n"
  "         c=='#' ||\n"
  "         c=='$' ||\n"
  "         c=='%' ||\n"
  "         c=='&' ||\n"
  "         c=='\\'' ||\n"
  "         c=='(' ||\n"
  "         c==')' ||\n"
  "         c=='*' ||\n"
  "         c=='+' ||\n"
  "         c==',' ||\n"
  "         c=='-' ||\n"
  "         c=='.' ||\n"
  "         c=='/' ||\n"
  "         c==':' ||\n"
  "         c==';' ||\n"
  "         c=='<' ||\n"
  "         c=='=' ||\n"
  "         c=='>' ||\n"
  "         c=='?' ||\n"
  "         c=='@' ||\n"
  "         c=='[' ||\n"
  "         c=='\\\\' ||\n"
  "         c==']' ||\n"
  "         c=='^' ||\n"
  "         c=='_' ||\n"
  "         c=='`' ||\n"
  "         c=='{' ||\n"
  "         c=='|' ||\n"
  "         c=='}' ||\n"
  "         c=='~'; }\n"
  "\n"
},
{ "c::isspace",
  "#line 1 \"<builtin-library>-isspace\"\n"
  "\n"
  "inline int isspace(int c)\n"
  "{ return c=='\\t' ||\n"
  "         c=='\\n' ||\n"
  "         c=='\\v' ||\n"
  "         c=='\\f' ||\n"
  "         c=='\\r' ||\n"
  "         c==' '; }\n"
  "\n"
},
{ "c::isupper",
  "#line 1 \"<builtin-library>-isupper\"\n"
  "\n"
  "inline int isupper(int c)\n"
  "{ return c>='A' && c<='Z'; }\n"
  "\n"
},
{ "c::isxdigit",
  "#line 1 \"<builtin-library>-isxdigit\"\n"
  "\n"
  "inline int isxdigit(int c)\n"
  "{ return (c>='A' && c<='F') || (c>='a' && c<='f') || (c>='0' && c<='9'); }\n"
  "\n"
},
{ "c::tolower",
  "#line 1 \"<builtin-library>-tolower\"\n"
  "\n"
  "inline int tolower(int c)\n"
  "{ return (c>='A' && c<='Z')?c+('a'-'A'):c; }\n"
  "\n"
},
{ "c::toupper",
  "#line 1 \"<builtin-library>-toupper\"\n"
  "\n"
  "inline int toupper(int c)\n"
  "{ return (c>='a' && c<='z')?c-('a'-'A'):c; }\n"
  "\n"
},
{ "c::err",
  "#line 1 \"<builtin-library>-err\"\n"
  "\n"
  "#ifndef __CPROVER_ERR_H_INCLUDED\n"
  "#include <err.h>\n"
  "#define __CPROVER_ERR_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "void err(int eval, const char *fmt, ...)\n"
  "{\n"
  "  // should check arguments\n"
  "}\n"
  "\n"
},
{ "c::err",
  "#line 1 \"<builtin-library>-err\"\n"
  "\n"
  "#ifndef __CPROVER_ERR_H_INCLUDED\n"
  "#include <err.h>\n"
  "#define __CPROVER_ERR_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "void errx(int eval, const char *fmt, ...)\n"
  "{\n"
  "  // should check arguments\n"
  "}\n"
  "\n"
},
{ "c::warn",
  "#line 1 \"<builtin-library>-warn\"\n"
  "\n"
  "#ifndef __CPROVER_ERR_H_INCLUDED\n"
  "#include <err.h>\n"
  "#define __CPROVER_ERR_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "void warn(const char *fmt, ...)\n"
  "{\n"
  "  // should check arguments\n"
  "}\n"
  "\n"
},
{ "c::warnx",
  "#line 1 \"<builtin-library>-warnx\"\n"
  "\n"
  "#ifndef __CPROVER_ERR_H_INCLUDED\n"
  "#include <err.h>\n"
  "#define __CPROVER_ERR_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "void warnx(const char *fmt, ...)\n"
  "{\n"
  "  // should check arguments\n"
  "}\n"
},
{ "c::fcntl",
  "#line 1 \"<builtin-library>-fcntl\"\n"
  "\n"
  "#ifndef __CPROVER_FCNTL_H_INCLUDED\n"
  "#include <fcntl.h>\n"
  "#define __CPROVER_FCNTL_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "int fcntl(int fd, int cmd, ...)\n"
  "{\n"
  "__CPROVER_hide:\n"
  "  int return_value;\n"
  "  return return_value;\n"
  "}\n"
},
{ "c::fegetround",
  "#line 1 \"<builtin-library>-fegetround\"\n"
  "\n"
  "inline int fegetround(void)\n"
  "{\n"
  "__CPROVER_hide:\n"
  "  return __CPROVER_rounding_mode;\n"
  "}\n"
  "\n"
},
{ "c::fesetround",
  "#line 1 \"<builtin-library>-fesetround\"\n"
  "\n"
  "inline int fesetround(int rounding_mode)\n"
  "{\n"
  "__CPROVER_hide:\n"
  "  __CPROVER_rounding_mode=rounding_mode;\n"
  "  return 0; // we never fail\n"
  "}\n"
},
{ "c::getopt",
  "#line 1 \"<builtin-library>-getopt\"\n"
  "\n"
  "extern char *optarg;\n"
  "\n"
  "inline int getopt(int argc, char * const argv[],\n"
  "                  const char *optstring)\n"
  "{\n"
  "  __CPROVER_HIDE:;\n"
  "  unsigned result_index;\n"
  "  __CPROVER_assume(result_index<argc);\n"
  "  #ifdef __CPROVER_STRING_ABSTRACTION\n"
  "  __CPROVER_assert(__CPROVER_is_zero_string(optstring),\n"
  "    \"getopt zero-termination of 3rd argument\");\n"
  "  #endif\n"
  "  optarg = argv[result_index];\n"
  "}\n"
},
{ "c::inet_addr",
  "#line 1 \"<builtin-library>-inet_addr\"\n"
  "\n"
  "#include <arpa/inet.h>\n"
  "\n"
  "in_addr_t inet_addr(const char *cp)\n"
  "{\n"
  "  __CPROVER_HIDE:;\n"
  "  #ifdef __CPROVER_STRING_ABSTRACTION\n"
  "  __CPROVER_assert(__CPROVER_is_zero_string(cp), \"inet_addr zero-termination of argument\");\n"
  "  #endif\n"
  "\n"
  "  in_addr_t result;\n"
  "  return result;\n"
  "}\n"
  "\n"
},
{ "c::inet_aton",
  "#line 1 \"<builtin-library>-inet_aton\"\n"
  "\n"
  "int inet_aton(const char *cp, struct in_addr *pin)\n"
  "{\n"
  "  __CPROVER_HIDE:;\n"
  "  #ifdef __CPROVER_STRING_ABSTRACTION\n"
  "  __CPROVER_assert(__CPROVER_is_zero_string(cp), \"inet_aton zero-termination of name argument\");\n"
  "  #endif\n"
  "\n"
  "  int result;\n"
  "  return result;\n"
  "}\n"
  "\n"
},
{ "c::inet_network",
  "#line 1 \"<builtin-library>-inet_network\"\n"
  "\n"
  "in_addr_t inet_network(const char *cp)\n"
  "{\n"
  "  __CPROVER_HIDE:;\n"
  "  #ifdef __CPROVER_STRING_ABSTRACTION\n"
  "  __CPROVER_assert(__CPROVER_is_zero_string(cp), \"inet_network zero-termination of name argument\");\n"
  "  #endif\n"
  "\n"
  "  in_addr_t result;\n"
  "  return result;\n"
  "}\n"
  "\n"
},
{ "c::fabs",
  "#line 1 \"<builtin-library>-fabs\"\n"
  "\n"
  "inline double fabs(double d) { return __CPROVER_fabs(d); }\n"
  "\n"
},
{ "c::fabsl",
  "#line 1 \"<builtin-library>-fabsl\"\n"
  "\n"
  "inline long double fabsl(long double d) { return __CPROVER_fabsl(d); }\n"
  "\n"
},
{ "c::fabsf",
  "#line 1 \"<builtin-library>-fabsf\"\n"
  "\n"
  "inline float fabsf(float f) { return __CPROVER_fabsf(f); }\n"
  "\n"
},
{ "c::isfinite",
  "#line 1 \"<builtin-library>-isfinite\"\n"
  "\n"
  "int isfinite(double d) { return __CPROVER_isfinite(d); }\n"
  "\n"
},
{ "c::isinf",
  "#line 1 \"<builtin-library>-isinf\"\n"
  "\n"
  "inline int isinf(double d) { return __CPROVER_isinf(d); }\n"
  "\n"
},
{ "c::isnan",
  "#line 1 \"<builtin-library>-isnan\"\n"
  "\n"
  "inline int isnan(double d) { return __CPROVER_isnan(d); }\n"
  "\n"
},
{ "c::isnormal",
  "#line 1 \"<builtin-library>-isnormal\"\n"
  "\n"
  "int isnormal(double d) { return __CPROVER_isnormal(d); }\n"
  "\n"
},
{ "c::signbit",
  "#line 1 \"<builtin-library>-signbit\"\n"
  "\n"
  "inline int signbit(double d) { return __CPROVER_sign(d); }\n"
  "\n"
},
{ "c::__signbitf",
  "#line 1 \"<builtin-library>-__signbitf\"\n"
  "\n"
  "inline float __signbitf(float f) { return __CPROVER_sign(f); }\n"
  "\n"
},
{ "c::__signbit",
  "#line 1 \"<builtin-library>-__signbit\"\n"
  "\n"
  "inline double __signbit(double d) { return __CPROVER_sign(d); }\n"
  "\n"
},
{ "c::__fpclassifyd",
  "#line 1 \"<builtin-library>-__fpclassifyd\"\n"
  "\n"
  "#ifndef __CPROVER_MATH_H_INCLUDED\n"
  "#include <math.h>\n"
  "#define __CPROVER_MATH_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "inline int __fpclassifyd(double d) {\n"
  "  if(__CPROVER_isnan(d)) return FP_NAN;\n"
  "  if(__CPROVER_isinf(d)) return FP_INFINITE;\n"
  "  if(d==0) return FP_ZERO;\n"
  "  if(__CPROVER_isnormal(d)) return FP_NORMAL;\n"
  "  return FP_SUBNORMAL;\n"
  "}\n"
  "\n"
},
{ "c::__fpclassifyf",
  "#line 1 \"<builtin-library>-__fpclassifyf\"\n"
  "\n"
  "#ifndef __CPROVER_MATH_H_INCLUDED\n"
  "#include <math.h>\n"
  "#define __CPROVER_MATH_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "inline int __fpclassifyf(float f) {\n"
  "  if(__CPROVER_isnan(f)) return FP_NAN;\n"
  "  if(__CPROVER_isinf(f)) return FP_INFINITE;\n"
  "  if(f==0) return FP_ZERO;\n"
  "  if(__CPROVER_isnormal(f)) return FP_NORMAL;\n"
  "  return FP_SUBNORMAL;\n"
  "}\n"
  "\n"
},
{ "c::__fpclassify",
  "#line 1 \"<builtin-library>-__fpclassify\"\n"
  "\n"
  "#ifndef __CPROVER_MATH_H_INCLUDED\n"
  "#include <math.h>\n"
  "#define __CPROVER_MATH_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "inline int __fpclassify(long double d) {\n"
  "  if(__CPROVER_isnan(d)) return FP_NAN;\n"
  "  if(__CPROVER_isinf(d)) return FP_INFINITE;\n"
  "  if(d==0) return FP_ZERO;\n"
  "  if(__CPROVER_isnormal(d)) return FP_NORMAL;\n"
  "  return FP_SUBNORMAL;\n"
  "}\n"
},
{ "c::gethostbyname",
  "#line 1 \"<builtin-library>-gethostbyname\"\n"
  "\n"
  "#include <netdb.h>\n"
  "\n"
  "struct hostent *gethostbyname(const char *name)\n"
  "{\n"
  "  __CPROVER_HIDE:;\n"
  "  #ifdef __CPROVER_STRING_ABSTRACTION\n"
  "  __CPROVER_assert(__CPROVER_is_zero_string(name), \"gethostbyname zero-termination of name argument\");\n"
  "  #endif\n"
  "\n"
  "  _Bool error;\n"
  "  if(error) return 0;\n"
  "  \n"
  "  // quite restrictive, as will alias between calls\n"
  "  static struct hostent result;\n"
  "  \n"
  "  // we whould be filling in the fields of this\n"
  "  return &result;\n"
  "}\n"
  "\n"
},
{ "c::gethostbyaddr",
  "#line 1 \"<builtin-library>-gethostbyaddr\"\n"
  "\n"
  "struct hostent *gethostbyaddr(const void *addr, socklen_t len, int type)\n"
  "{\n"
  "  __CPROVER_HIDE:;\n"
  "\n"
  "  _Bool error;\n"
  "  if(error) return 0;\n"
  "  \n"
  "  // quite restrictive, as will alias between calls\n"
  "  static struct hostent result;\n"
  "  \n"
  "  // we whould be filling in the fields of this\n"
  "  return &result;\n"
  "}\n"
  "\n"
},
{ "c::gethostent",
  "#line 1 \"<builtin-library>-gethostent\"\n"
  "\n"
  "struct hostent *gethostent(void)\n"
  "{\n"
  "  __CPROVER_HIDE:;\n"
  "\n"
  "  _Bool error;\n"
  "  if(error) return 0;\n"
  "  \n"
  "  // quite restrictive, as will alias between calls\n"
  "  static struct hostent result;\n"
  "  \n"
  "  // we whould be filling in the fields of this\n"
  "  return &result;\n"
  "}\n"
},
{ "c::__new",
  "#line 1 \"<builtin-library>-__new\"\n"
  "\n"
  "inline void *__new(__typeof__(sizeof(int)) malloc_size)\n"
  "{\n"
  "  // The constructor call is done by the front-end.\n"
  "  // This just does memory allocation.\n"
  "  __CPROVER_HIDE:;\n"
  "  void *res;\n"
  "  res=__CPROVER_malloc(malloc_size);\n"
  "\n"
  "  // ensure it's not recorded as deallocated\n"
  "  __CPROVER_deallocated=(res==__CPROVER_deallocated)?0:__CPROVER_deallocated;\n"
  "  \n"
  "  // record the object size for non-determistic bounds checking\n"
  "  _Bool record_malloc;\n"
  "  if(record_malloc)\n"
  "  {\n"
  "    __CPROVER_malloc_object=res;\n"
  "    __CPROVER_malloc_size=malloc_size;\n"
  "  }\n"
  "  \n"
  "  return res;\n"
  "}\n"
  "\n"
},
{ "c::__placement_new",
  "#line 1 \"<builtin-library>-__placement_new\"\n"
  "\n"
  "inline void *__placement_new(__typeof__(sizeof(int)) malloc_size, void *p)\n"
  "{\n"
  "  // The constructor call is done by the front-end.\n"
  "  __CPROVER_HIDE:;\n"
  "  return p;\n"
  "}\n"
  "\n"
},
{ "c::__delete",
  "#line 1 \"<builtin-library>-__delete\"\n"
  "\n"
  "inline void __delete(void *ptr)\n"
  "{\n"
  "  __CPROVER_HIDE:;\n"
  "  // If ptr is NULL, no operation is performed.\n"
  "  // This is a requirement by the standard, not generosity!\n"
  "  if(ptr!=0)\n"
  "  {\n"
  "    // is it dynamic?\n"
  "    __CPROVER_assert(__CPROVER_DYNAMIC_OBJECT(ptr),\n"
  "                     \"delete argument must be dynamic object\");\n"
  "    __CPROVER_assert(__CPROVER_POINTER_OFFSET(ptr)==0,\n"
  "                     \"delete argument must have offset zero\");\n"
  "\n"
  "    // catch double delete\n"
  "    __CPROVER_assert(__CPROVER_deallocated!=ptr, \"double delete\");\n"
  "    \n"
  "    // non-deterministically record as deallocated\n"
  "    __CPROVER_deallocated=record?ptr:__CPROVER_deallocated;\n"
  "  }\n"
  "}\n"
  "\n"
},
{ "c::__noop",
  "#line 1 \"<builtin-library>-__noop\"\n"
  "\n"
  "int __noop()\n"
  "{\n"
  "  // does nothing\n"
  "}\n"
},
{ "c::pthread_mutex_init",
  "#line 1 \"<builtin-library>-pthread_mutex_init\"\n"
  "\n"
  "#ifndef __CPROVER_PTHREAD_H_INCLUDED\n"
  "#include <pthread.h>\n"
  "#define __CPROVER_PTHREAD_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "inline int pthread_mutex_init(\n"
  "  pthread_mutex_t *mutex, const pthread_mutexattr_t *mutexattr)\n"
  "{ __CPROVER_HIDE: *((char *)mutex)=0; return 0; }\n"
  "\n"
},
{ "c::pthread_mutex_lock",
  "#line 1 \"<builtin-library>-pthread_mutex_lock\"\n"
  "\n"
  "#ifndef __CPROVER_PTHREAD_H_INCLUDED\n"
  "#include <pthread.h>\n"
  "#define __CPROVER_PTHREAD_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "inline int pthread_mutex_lock(pthread_mutex_t *mutex)\n"
  "{ __CPROVER_HIDE:\n"
  "  __CPROVER_atomic_begin();\n"
  "  __CPROVER_assume(!*((char *)mutex));\n"
  "  *((char *)mutex)=1;\n"
  "  __CPROVER_atomic_end();\n"
  "  return 0; // we never fail\n"
  "}\n"
  "\n"
},
{ "c::pthread_mutex_trylock",
  "#line 1 \"<builtin-library>-pthread_mutex_trylock\"\n"
  "\n"
  "#ifndef __CPROVER_PTHREAD_H_INCLUDED\n"
  "#include <pthread.h>\n"
  "#define __CPROVER_PTHREAD_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "inline int pthread_mutex_trylock(pthread_mutex_t *mutex)\n"
  "{\n"
  "  __CPROVER_HIDE:\n"
  "  __CPROVER_atomic_begin();\n"
  "  if(*((char *)mutex)) { __CPROVER_atomic_end(); return 1; }\n"
  "  *((char *)mutex)=1;\n"
  "  __CPROVER_atomic_end();\n"
  "  return 0;\n"
  "}\n"
  "\n"
},
{ "c::pthread_mutex_unlock",
  "#line 1 \"<builtin-library>-pthread_mutex_unlock\"\n"
  "\n"
  "#ifndef __CPROVER_PTHREAD_H_INCLUDED\n"
  "#include <pthread.h>\n"
  "#define __CPROVER_PTHREAD_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "inline int pthread_mutex_unlock(pthread_mutex_t *mutex)\n"
  "{ __CPROVER_HIDE:\n"
  "  __CPROVER_assert(*((char *)mutex),\n"
  "    \"must hold lock upon unlock\");\n"
  "  *((char *)mutex)=0;\n"
  "  return 0; // we never fail\n"
  "}\n"
  "\n"
},
{ "c::pthread_mutex_destroy",
  "#line 1 \"<builtin-library>-pthread_mutex_destroy\"\n"
  "\n"
  "#ifndef __CPROVER_PTHREAD_H_INCLUDED\n"
  "#include <pthread.h>\n"
  "#define __CPROVER_PTHREAD_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "inline int pthread_mutex_destroy(pthread_mutex_t *mutex)\n"
  "{ }\n"
  "\n"
},
{ "c::pthread_exit",
  "#line 1 \"<builtin-library>-pthread_exit\"\n"
  "\n"
  "#ifndef __CPROVER_PTHREAD_H_INCLUDED\n"
  "#include <pthread.h>\n"
  "#define __CPROVER_PTHREAD_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "inline void pthread_exit(void *value_ptr)\n"
  "{ __CPROVER_hide:; __CPROVER_assume(0); }\n"
  "\n"
},
{ "c::pthread_rwlock_destroy",
  "#line 1 \"<builtin-library>-pthread_rwlock_destroy\"\n"
  "\n"
  "#ifndef __CPROVER_PTHREAD_H_INCLUDED\n"
  "#include <pthread.h>\n"
  "#define __CPROVER_PTHREAD_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "inline int pthread_rwlock_destroy(pthread_rwlock_t *lock)\n"
  "{ }\n"
  "\n"
},
{ "c::pthread_rwlock_init",
  "#line 1 \"<builtin-library>-pthread_rwlock_init\"\n"
  "\n"
  "#ifndef __CPROVER_PTHREAD_H_INCLUDED\n"
  "#include <pthread.h>\n"
  "#define __CPROVER_PTHREAD_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "inline int pthread_rwlock_init(pthread_rwlock_t *lock, \n"
  "  const pthread_rwlockattr_t *attr)\n"
  "{ __CPROVER_HIDE: (*(char *)lock)=0; }\n"
  "\n"
},
{ "c::pthread_rwlock_rdlock",
  "#line 1 \"<builtin-library>-pthread_rwlock_rdlock\"\n"
  "\n"
  "#ifndef __CPROVER_PTHREAD_H_INCLUDED\n"
  "#include <pthread.h>\n"
  "#define __CPROVER_PTHREAD_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "inline int pthread_rwlock_rdlock(pthread_rwlock_t *lock)\n"
  "{ /* TODO */ }\n"
  "\n"
},
{ "c::pthread_rwlock_tryrdlock",
  "#line 1 \"<builtin-library>-pthread_rwlock_tryrdlock\"\n"
  "\n"
  "#ifndef __CPROVER_PTHREAD_H_INCLUDED\n"
  "#include <pthread.h>\n"
  "#define __CPROVER_PTHREAD_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "inline int pthread_rwlock_tryrdlock(pthread_rwlock_t *lock)\n"
  "{ /* TODO */ }\n"
  "\n"
},
{ "c::pthread_rwlock_trywrlock",
  "#line 1 \"<builtin-library>-pthread_rwlock_trywrlock\"\n"
  "\n"
  "#ifndef __CPROVER_PTHREAD_H_INCLUDED\n"
  "#include <pthread.h>\n"
  "#define __CPROVER_PTHREAD_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "inline int pthread_rwlock_trywrlock(pthread_rwlock_t *lock)\n"
  "{ __CPROVER_HIDE:\n"
  "  __CPROVER_atomic_begin();\n"
  "  if(*(char *)lock) { __CPROVER_atomic_end(); return 1; }\n"
  "  (*(char *)lock)=1;\n"
  "  __CPROVER_atomic_end();\n"
  "  return 0;\n"
  "}\n"
  "\n"
},
{ "c::pthread_rwlock_unlock",
  "#line 1 \"<builtin-library>-pthread_rwlock_unlock\"\n"
  "\n"
  "#ifndef __CPROVER_PTHREAD_H_INCLUDED\n"
  "#include <pthread.h>\n"
  "#define __CPROVER_PTHREAD_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "inline int pthread_rwlock_unlock(pthread_rwlock_t *lock)\n"
  "{ __CPROVER_HIDE: (*(char *)lock)=0; }\n"
  "\n"
},
{ "c::pthread_rwlock_wrlock",
  "#line 1 \"<builtin-library>-pthread_rwlock_wrlock\"\n"
  "\n"
  "#ifndef __CPROVER_PTHREAD_H_INCLUDED\n"
  "#include <pthread.h>\n"
  "#define __CPROVER_PTHREAD_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "inline int pthread_rwlock_wrlock(pthread_rwlock_t *lock)\n"
  "{ __CPROVER_HIDE:\n"
  "  __CPROVER_atomic_begin();\n"
  "  __CPROVER_assume(!(*(char *)lock));\n"
  "  (*(char *)lock)=1;\n"
  "  __CPROVER_atomic_end();\n"
  "  return 0; // we never fail\n"
  "}\n"
  "\n"
},
{ "c::pthread_create",
  "#line 1 \"<builtin-library>-pthread_create\"\n"
  "\n"
  "#ifndef __CPROVER_PTHREAD_H_INCLUDED\n"
  "#include <pthread.h>\n"
  "#define __CPROVER_PTHREAD_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "inline int pthread_create(\n"
  "  pthread_t *thread,\n"
  "  pthread_attr_t *attr,\n"
  "  void * (*start_routine)(void *),\n"
  "  void *arg)\n"
  "{\n"
  "  __CPROVER_HIDE:;\n"
  "  pthread_t thread_id;\n"
  "\n"
  "  if(!thread) *thread=thread_id;\n"
  "  __CPROVER_ASYNC_1: start_routine(arg);\n"
  "\n"
  "  return 0;\n"
  "}\n"
  "\n"
},
{ "c::kill",
  "#line 1 \"<builtin-library>-kill\"\n"
  "\n"
  "#ifndef __CPROVER_SYS_TYPES_H_INCLUDED\n"
  "#include <sys/types.h>\n"
  "#define __CPROVER_SYS_TYPES_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "#ifndef __CPROVER_SIGNAL_H_INCLUDED\n"
  "#include <signal.h>\n"
  "#define __CPROVER_SIGNAL_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "int kill(pid_t pid, int sig)\n"
  "{\n"
  "}\n"
  "\n"
},
{ "c::putchar",
  "#line 1 \"<builtin-library>-putchar\"\n"
  "\n"
  "#ifndef __CPROVER_STDIO_H_INCLUDED\n"
  "#include <stdio.h>\n"
  "#define __CPROVER_STDIO_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "inline int putchar(int c)\n"
  "{\n"
  "  _Bool error;\n"
  "  __CPROVER_HIDE: printf(\"%c\", c);\n"
  "  return (error?-1:c);\n"
  "}\n"
  "\n"
},
{ "c::puts",
  "#line 1 \"<builtin-library>-puts\"\n"
  "\n"
  "#ifndef __CPROVER_STDIO_H_INCLUDED\n"
  "#include <stdio.h>\n"
  "#define __CPROVER_STDIO_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "inline int puts(const char *s)\n"
  "{\n"
  "  _Bool error;\n"
  "  int ret;\n"
  "  __CPROVER_HIDE: printf(\"%s\\n\", s);\n"
  "  if(error) ret=-1; else __CPROVER_assume(ret>=0);\n"
  "  return ret;\n"
  "}\n"
  "\n"
},
{ "c::fopen",
  "#line 1 \"<builtin-library>-fopen\"\n"
  "\n"
  "#ifndef __CPROVER_STDIO_H_INCLUDED\n"
  "#include <stdio.h>\n"
  "#define __CPROVER_STDIO_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "#ifndef __CPROVER_STDLIB_H_INCLUDED\n"
  "#include <stdlib.h>\n"
  "#define __CPROVER_STDLIB_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "inline FILE *fopen(const char *filename, const char *mode)\n"
  "{\n"
  "  __CPROVER_HIDE:;\n"
  "  #ifdef __CPROVER_STRING_ABSTRACTION\n"
  "  __CPROVER_assert(__CPROVER_is_zero_string(filename), \"fopen zero-termination of 1st argument\");\n"
  "  __CPROVER_assert(__CPROVER_is_zero_string(mode), \"fopen zero-termination of 2nd argument\");\n"
  "  #endif\n"
  "\n"
  "  FILE *f=malloc(sizeof(FILE));\n"
  "\n"
  "  return f;\n"
  "}\n"
  "\n"
},
{ "c::fclose",
  "#line 1 \"<builtin-library>-fclose\"\n"
  "\n"
  "#ifndef __CPROVER_STDIO_H_INCLUDED\n"
  "#include <stdio.h>\n"
  "#define __CPROVER_STDIO_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "inline int fclose(FILE *stream)\n"
  "{\n"
  "  __CPROVER_HIDE:;\n"
  "  int return_value;\n"
  "  free(stream);\n"
  "  return return_value;\n"
  "}\n"
  "\n"
},
{ "c::fdopen",
  "#line 1 \"<builtin-library>-fdopen\"\n"
  "\n"
  "#ifndef __CPROVER_STDIO_H_INCLUDED\n"
  "#include <stdio.h>\n"
  "#define __CPROVER_STDIO_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "#ifndef __CPROVER_STDLIB_H_INCLUDED\n"
  "#include <stdlib.h>\n"
  "#define __CPROVER_STDLIB_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "inline FILE *fdopen(int handle, const char *mode)\n"
  "{\n"
  "  __CPROVER_HIDE:;\n"
  "  #ifdef __CPROVER_STRING_ABSTRACTION\n"
  "  __CPROVER_assert(__CPROVER_is_zero_string(mode),\n"
  "    \"fdopen zero-termination of 2nd argument\");\n"
  "  #endif\n"
  "\n"
  "  FILE *f=malloc(sizeof(FILE));\n"
  "\n"
  "  return f;\n"
  "}\n"
  "\n"
},
{ "c::fgets",
  "#line 1 \"<builtin-library>-fgets\"\n"
  "\n"
  "#ifndef __CPROVER_STDIO_H_INCLUDED\n"
  "#include <stdio.h>\n"
  "#define __CPROVER_STDIO_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "inline char *fgets(char *str, int size, FILE *stream)\n"
  "{\n"
  "  __CPROVER_HIDE:;\n"
  "  _Bool error;\n"
  "\n"
  "  #ifdef __CPROVER_STRING_ABSTRACTION\n"
  "  int resulting_size;\n"
  "  __CPROVER_assert(__CPROVER_buffer_size(str)>=size, \"buffer-overflow in fgets\");\n"
  "  if(size>0)\n"
  "  {\n"
  "    __CPROVER_assume(resulting_size<size);\n"
  "    __CPROVER_is_zero_string(str)=!error;\n"
  "    __CPROVER_zero_string_length(str)=resulting_size;\n"
  "  }\n"
  "  #endif\n"
  "\n"
  "  return error?0:str;\n"
  "}\n"
  "\n"
},
{ "c::fread",
  "#line 1 \"<builtin-library>-fread\"\n"
  "\n"
  "#ifndef __CPROVER_STDIO_H_INCLUDED\n"
  "#include <stdio.h>\n"
  "#define __CPROVER_STDIO_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "inline size_t fread(\n"
  "  void *ptr,\n"
  "  size_t size,\n"
  "  size_t nitems,\n"
  "  FILE *stream)\n"
  "{\n"
  "  __CPROVER_HIDE:;\n"
  "  size_t nread;\n"
  "  size_t bytes=nread*size;\n"
  "  size_t i;\n"
  "  __CPROVER_assume(nread<=nitems);\n"
  "\n"
  "  for(i=0; i<bytes; i++)\n"
  "  {\n"
  "    char nondet_char;\n"
  "    ((char *)ptr)[i]=nondet_char;\n"
  "  }\n"
  "\n"
  "  return nread;\n"
  "}\n"
  "\n"
},
{ "c::feof",
  "#line 1 \"<builtin-library>-feof\"\n"
  "\n"
  "#ifndef __CPROVER_STDIO_H_INCLUDED\n"
  "#include <stdio.h>\n"
  "#define __CPROVER_STDIO_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "inline int feof(FILE *stream)\n"
  "{\n"
  "  // just return nondet\n"
  "  int return_value;\n"
  "  *stream;\n"
  "  return return_value;\n"
  "}\n"
  "\n"
},
{ "c::ferror",
  "#line 1 \"<builtin-library>-ferror\"\n"
  "\n"
  "#ifndef __CPROVER_STDIO_H_INCLUDED\n"
  "#include <stdio.h>\n"
  "#define __CPROVER_STDIO_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "inline int ferror(FILE *stream)\n"
  "{\n"
  "  // just return nondet\n"
  "  int return_value;\n"
  "  *stream;\n"
  "  return return_value;\n"
  "}\n"
  "\n"
},
{ "c::fileno",
  "#line 1 \"<builtin-library>-fileno\"\n"
  "\n"
  "#ifndef __CPROVER_STDIO_H_INCLUDED\n"
  "#include <stdio.h>\n"
  "#define __CPROVER_STDIO_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "inline int fileno(FILE *stream)\n"
  "{\n"
  "  // just return nondet\n"
  "  int return_value;\n"
  "  *stream;\n"
  "  return return_value;\n"
  "}\n"
  "\n"
},
{ "c::fputs",
  "#line 1 \"<builtin-library>-fputs\"\n"
  "\n"
  "#ifndef __CPROVER_STDIO_H_INCLUDED\n"
  "#include <stdio.h>\n"
  "#define __CPROVER_STDIO_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "int fputs(const char *s, FILE *stream)\n"
  "{\n"
  "  // just return nondet\n"
  "  int return_value;\n"
  "  #ifdef __CPROVER_STRING_ABSTRACTION\n"
  "  __CPROVER_assert(__CPROVER_is_zero_string(s), \"fputs zero-termination of 1st argument\");\n"
  "  #endif\n"
  "  *stream;\n"
  "  return return_value;\n"
  "}\n"
  "\n"
},
{ "c::fflush",
  "#line 1 \"<builtin-library>-fflush\"\n"
  "\n"
  "#ifndef __CPROVER_STDIO_H_INCLUDED\n"
  "#include <stdio.h>\n"
  "#define __CPROVER_STDIO_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "int fflush(FILE *stream)\n"
  "{\n"
  "  // just return nondet\n"
  "  int return_value;\n"
  "  *stream;\n"
  "  return return_value;\n"
  "}\n"
  "\n"
},
{ "c::fpurge",
  "#line 1 \"<builtin-library>-fpurge\"\n"
  "\n"
  "#ifndef __CPROVER_STDIO_H_INCLUDED\n"
  "#include <stdio.h>\n"
  "#define __CPROVER_STDIO_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "int fpurge(FILE *stream)\n"
  "{\n"
  "  // just return nondet\n"
  "  int return_value;\n"
  "  *stream;\n"
  "  return return_value;\n"
  "}\n"
  "\n"
},
{ "c::read",
  "#line 1 \"<builtin-library>-read\"\n"
  "\n"
  "#ifndef __CPROVER_UNISTD_H_INCLUDED\n"
  "#include <unistd.h>\n"
  "#define __CPROVER_UNISTD_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "inline ssize_t read(int fildes, void *buf, size_t nbyte)\n"
  "{\n"
  "  __CPROVER_HIDE:;\n"
  "  ssize_t nread;\n"
  "  size_t i;\n"
  "  __CPROVER_assume(nread<=nbyte);\n"
  "\n"
  "  for(i=0; i<nbyte; i++)\n"
  "  {\n"
  "    char nondet_char;\n"
  "    ((char *)buf)[i]=nondet_char;\n"
  "  }\n"
  "\n"
  "  return nread;\n"
  "}\n"
  "\n"
},
{ "c::fgetc",
  "#line 1 \"<builtin-library>-fgetc\"\n"
  "\n"
  "#ifndef __CPROVER_STDIO_H_INCLUDED\n"
  "#include <stdio.h>\n"
  "#define __CPROVER_STDIO_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "inline int fgetc(FILE *stream)\n"
  "{\n"
  "  __CPROVER_HIDE:;\n"
  "  int return_value;\n"
  "  *stream;\n"
  "  // it's a byte or EOF (-1)\n"
  "  __CPROVER_assume(return_value>=-1 && return_value<=255);\n"
  "  return return_value;\n"
  "}\n"
  "\n"
},
{ "c::getc",
  "#line 1 \"<builtin-library>-getc\"\n"
  "\n"
  "#ifndef __CPROVER_STDIO_H_INCLUDED\n"
  "#include <stdio.h>\n"
  "#define __CPROVER_STDIO_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "inline int getc(FILE *stream)\n"
  "{\n"
  "  __CPROVER_HIDE:;\n"
  "  int return_value;\n"
  "  *stream;\n"
  "  // it's a byte or EOF\n"
  "  __CPROVER_assume(return_value>=-1 && return_value<=255);\n"
  "  return return_value;\n"
  "}\n"
  "\n"
},
{ "c::getchar",
  "#line 1 \"<builtin-library>-getchar\"\n"
  "\n"
  "#ifndef __CPROVER_STDIO_H_INCLUDED\n"
  "#include <stdio.h>\n"
  "#define __CPROVER_STDIO_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "inline int getchar()\n"
  "{\n"
  "  __CPROVER_HIDE:;\n"
  "  int return_value;\n"
  "  // it's a byte or EOF\n"
  "  __CPROVER_assume(return_value>=-1 && return_value<=255);\n"
  "  return return_value;\n"
  "}\n"
  "\n"
},
{ "c::getw",
  "#line 1 \"<builtin-library>-getw\"\n"
  "\n"
  "#ifndef __CPROVER_STDIO_H_INCLUDED\n"
  "#include <stdio.h>\n"
  "#define __CPROVER_STDIO_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "inline int getw(FILE *stream)\n"
  "{\n"
  "  __CPROVER_HIDE:;\n"
  "  int return_value;\n"
  "  *stream;\n"
  "  // it's any int, no restriction\n"
  "  return return_value;\n"
  "}\n"
  "\n"
},
{ "c::fseek",
  "#line 1 \"<builtin-library>-fseek\"\n"
  "\n"
  "#ifndef __CPROVER_STDIO_H_INCLUDED\n"
  "#include <stdio.h>\n"
  "#define __CPROVER_STDIO_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "inline int fseek(FILE *stream, long offset, int whence)\n"
  "{\n"
  "  __CPROVER_HIDE:;\n"
  "  int return_value;\n"
  "  *stream;\n"
  "  return return_value;\n"
  "}\n"
  "\n"
},
{ "c::ftell",
  "#line 1 \"<builtin-library>-ftell\"\n"
  "\n"
  "#ifndef __CPROVER_STDIO_H_INCLUDED\n"
  "#include <stdio.h>\n"
  "#define __CPROVER_STDIO_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "long ftell(FILE *stream)\n"
  "{\n"
  "  __CPROVER_HIDE:;\n"
  "  int return_value;\n"
  "  *stream;\n"
  "  return return_value;\n"
  "}\n"
  "\n"
},
{ "c::rewind",
  "#line 1 \"<builtin-library>-rewind\"\n"
  "\n"
  "#ifndef __CPROVER_STDIO_H_INCLUDED\n"
  "#include <stdio.h>\n"
  "#define __CPROVER_STDIO_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "void rewind(FILE *stream)\n"
  "{\n"
  "  __CPROVER_HIDE:\n"
  "  *stream;\n"
  "}\n"
  "\n"
},
{ "c::fwrite",
  "#line 1 \"<builtin-library>-fwrite\"\n"
  "\n"
  "#ifndef __CPROVER_STDIO_H_INCLUDED\n"
  "#include <stdio.h>\n"
  "#define __CPROVER_STDIO_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "size_t fwrite(\n"
  "  const void *ptr,\n"
  "  size_t size,\n"
  "  size_t nitems,\n"
  "  FILE *stream)\n"
  "{\n"
  "  __CPROVER_HIDE:;\n"
  "  *stream;\n"
  "  size_t nwrite;\n"
  "  __CPROVER_assume(nwrite<=nitems);\n"
  "  return nwrite;\n"
  "}\n"
  "\n"
},
{ "c::perror",
  "#line 1 \"<builtin-library>-perror\"\n"
  "\n"
  "#ifndef __CPROVER_STDIO_H_INCLUDED\n"
  "#include <stdio.h>\n"
  "#define __CPROVER_STDIO_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "void perror(const char *s)\n"
  "{\n"
  "  __CPROVER_hide:;\n"
  "  if(s!=0)\n"
  "  {\n"
  "    #ifdef __CPROVER_STRING_ABSTRACTION\n"
  "    __CPROVER_assert(__CPROVER_is_zero_string(s), \"perror zero-termination\");\n"
  "    #endif\n"
  "    // should go to stderr\n"
  "    if(s[0]!=0)\n"
  "      printf(\"%s: \", s);\n"
  "  }\n"
  "  \n"
  "  // TODO: print errno error\n"
  "}\n"
  "\n"
},
{ "c::abs",
  "#line 1 \"<builtin-library>-abs\"\n"
  "\n"
  "#undef abs\n"
  "\n"
  "inline int abs(int i) { return __CPROVER_abs(i); }\n"
  "\n"
},
{ "c::labs",
  "#line 1 \"<builtin-library>-labs\"\n"
  "\n"
  "#undef labs\n"
  "\n"
  "inline long int labs(long int i) { return __CPROVER_labs(i); }\n"
  "\n"
},
{ "c::exit",
  "#line 1 \"<builtin-library>-exit\"\n"
  "\n"
  "#undef exit\n"
  "\n"
  "inline void exit(int status)\n"
  "{\n"
  "  __CPROVER_assume(0);\n"
  "}\n"
  "\n"
},
{ "c::abort",
  "#line 1 \"<builtin-library>-abort\"\n"
  "\n"
  "#undef abort\n"
  "\n"
  "inline void abort(void)\n"
  "{\n"
  "  __CPROVER_assume(0);\n"
  "}\n"
  "\n"
},
{ "c::calloc",
  "#line 1 \"<builtin-library>-calloc\"\n"
  "\n"
  "#undef calloc\n"
  "\n"
  "inline void *calloc(__CPROVER_size_t nmemb, __CPROVER_size_t size)\n"
  "{\n"
  "  __CPROVER_HIDE:;\n"
  "  __CPROVER_size_t total_size=nmemb*size;\n"
  "  void *res;\n"
  "  res=malloc(total_size);\n"
  "  #ifdef __CPROVER_STRING_ABSTRACTION\n"
  "  __CPROVER_is_zero_string(res);\n"
  "  __CPROVER_zero_string_length(res)=0;\n"
  "  //for(int i=0; i<nmemb*size; i++) res[i]=0;\n"
  "  #else\n"
  "  // there should be memset here\n"
  "  //char *p=res;\n"
  "  //for(int i=0; i<total_size; i++) p[i]=0;\n"
  "  #endif\n"
  "  return res;\n"
  "}\n"
  "\n"
},
{ "c::malloc",
  "#line 1 \"<builtin-library>-malloc\"\n"
  "\n"
  "inline void *malloc(__CPROVER_size_t malloc_size)\n"
  "{\n"
  "  // realistically, malloc may return NULL,\n"
  "  // and __CPROVER_malloc doesn't, but no one cares\n"
  "  __CPROVER_HIDE:;\n"
  "  void *res;\n"
  "  res=__CPROVER_malloc(malloc_size);\n"
  "\n"
  "  // make sure it's not recorded as deallocated\n"
  "  __CPROVER_deallocated=(res==__CPROVER_deallocated)?0:__CPROVER_deallocated;\n"
  "  \n"
  "  // record the object size for non-determistic bounds checking\n"
  "  _Bool record_malloc;\n"
  "  __CPROVER_malloc_object=record_malloc?res:__CPROVER_malloc_object;\n"
  "  __CPROVER_malloc_size=record_malloc?malloc_size:__CPROVER_malloc_size;\n"
  "  \n"
  "  return res;\n"
  "}\n"
  "\n"
},
{ "c::free",
  "#line 1 \"<builtin-library>-free\"\n"
  "\n"
  "#undef free\n"
  "\n"
  "inline void free(void *ptr)\n"
  "{\n"
  "  __CPROVER_HIDE:;\n"
  "  // If ptr is NULL, no operation is performed.\n"
  "  if(ptr!=0)\n"
  "  {\n"
  "    // is it dynamic?\n"
  "    __CPROVER_assert(__CPROVER_DYNAMIC_OBJECT(ptr),\n"
  "                     \"free argument is dynamic object\");\n"
  "    __CPROVER_assert(__CPROVER_POINTER_OFFSET(ptr)==0,\n"
  "                     \"free argument has offset zero\");\n"
  "\n"
  "    // catch double free\n"
  "    if(__CPROVER_deallocated==ptr)\n"
  "      __CPROVER_assert(0, \"double free\");\n"
  "    \n"
  "    // non-deterministically record as deallocated\n"
  "    _Bool record;\n"
  "    if(record) __CPROVER_deallocated=ptr;\n"
  "  }\n"
  "}\n"
  "\n"
},
{ "c::atoi",
  "#line 1 \"<builtin-library>-atoi\"\n"
  "\n"
  "#undef atoi\n"
  "\n"
  "inline int atoi(const char *nptr)\n"
  "{\n"
  "  __CPROVER_HIDE:;\n"
  "  int res;\n"
  "  #ifdef __CPROVER_STRING_ABSTRACTION\n"
  "  __CPROVER_assert(__CPROVER_is_zero_string(nptr),\n"
  "    \"zero-termination of argument of atoi\");\n"
  "  #endif\n"
  "  return res;\n"
  "}\n"
  "\n"
},
{ "c::atol",
  "#line 1 \"<builtin-library>-atol\"\n"
  "\n"
  "#undef atol\n"
  "\n"
  "inline long atol(const char *nptr)\n"
  "{\n"
  "  __CPROVER_HIDE:;\n"
  "  long res;\n"
  "  #ifdef __CPROVER_STRING_ABSTRACTION\n"
  "  __CPROVER_assert(__CPROVER_is_zero_string(nptr),\n"
  "    \"zero-termination of argument of atol\");\n"
  "  #endif\n"
  "  return res;\n"
  "}\n"
  "\n"
},
{ "c::getenv",
  "#line 1 \"<builtin-library>-getenv\"\n"
  "\n"
  "#undef getenv\n"
  "\n"
  "inline char *getenv(const char *name)\n"
  "{\n"
  "  __CPROVER_HIDE:;\n"
  "\n"
  "  #ifdef __CPROVER_STRING_ABSTRACTION\n"
  "  __CPROVER_assert(__CPROVER_is_zero_string(name),\n"
  "    \"zero-termination of argument of getenv\");\n"
  "  #endif\n"
  "\n"
  "  _Bool found;\n"
  "  if(!found) return 0;\n"
  "\n"
  "  char *buffer;\n"
  "  __CPROVER_size_t buf_size;\n"
  "\n"
  "  __CPROVER_assume(buf_size>=1);\n"
  "  buffer=(char *)__CPROVER_malloc(buf_size);\n"
  "  buffer[buf_size-1]=0;\n"
  "  return buffer;\n"
  "}\n"
},
{ "c::__builtin___strcpy_chk",
  "#line 1 \"<builtin-library>-__builtin___strcpy_chk\"\n"
  "\n"
  "inline char *__builtin___strcpy_chk(char *dst, const char *src, __CPROVER_size_t s)\n"
  "{\n"
  "  __CPROVER_HIDE:;\n"
  "  #ifdef __CPROVER_STRING_ABSTRACTION\n"
  "  __CPROVER_assert(__CPROVER_is_zero_string(src), \"strcpy zero-termination of 2nd argument\");\n"
  "  __CPROVER_assert(__CPROVER_buffer_size(dst)>__CPROVER_zero_string_length(src), \"strcpy buffer overflow\");\n"
  "  dst[__CPROVER_zero_string_length(src)]=0;\n"
  "  __CPROVER_is_zero_string(dst)=1;\n"
  "  __CPROVER_zero_string_length(dst)=__CPROVER_zero_string_length(src);\n"
  "  #else\n"
  "  __CPROVER_size_t i=0;\n"
  "  char ch;\n"
  "  do\n"
  "  {\n"
  "    ch=src[i];\n"
  "    dst[i]=ch;\n"
  "    i++;\n"
  "  }\n"
  "  while(ch!=(char)0);\n"
  "  #endif\n"
  "  return dst;\n"
  "}\n"
  "\n"
},
{ "c::__builtin___strcat_chk",
  "#line 1 \"<builtin-library>-__builtin___strcat_chk\"\n"
  "\n"
  "__inline char *__builtin___strcat_chk(char *dst, const char *src, __CPROVER_size_t s)\n"
  "{\n"
  "  __CPROVER_HIDE:;\n"
  "  #ifdef __CPROVER_STRING_ABSTRACTION\n"
  "  __CPROVER_size_t new_size;\n"
  "  __CPROVER_assert(__CPROVER_is_zero_string(dst), \"strcat zero-termination of 1st argument\");\n"
  "  __CPROVER_assert(__CPROVER_is_zero_string(src), \"strcat zero-termination of 2nd argument\");\n"
  "  new_size=__CPROVER_zero_string_length(dst)+__CPROVER_zero_string_length(src);\n"
  "  __CPROVER_assert(__CPROVER_buffer_size(dst)>new_size,\n"
  "                   \"strcat buffer overflow\");\n"
  "  __CPROVER_size_t old_size=__CPROVER_zero_string_length(dst);\n"
  "  //\"  for(size_t i=0; i<__CPROVER_zero_string_length(src); i++)\n"
  "  //\"    dst[old_size+i];\n"
  "  dst[new_size]=0;\n"
  "  __CPROVER_is_zero_string(dst)=1;\n"
  "  __CPROVER_zero_string_length(dst)=new_size;\n"
  "  #else\n"
  "  __CPROVER_size_t i=0;\n"
  "  while(dst[i]!=0) i++;\n"
  "\n"
  "  __CPROVER_size_t j=0;\n"
  "  char ch;\n"
  "  do\n"
  "  {\n"
  "    char ch=src[j];\n"
  "    dst[i]=ch;\n"
  "    i++;\n"
  "    j++;\n"
  "  }\n"
  "  while(ch!=(char)0);\n"
  "  #endif\n"
  "  return dst;\n"
  "}                        \n"
  "\n"
},
{ "c::__builtin___strncat_chk",
  "#line 1 \"<builtin-library>-__builtin___strncat_chk\"\n"
  "\n"
  "__inline char *__builtin___strncat_chk(\n"
  "  char *dest, const char *src, __CPROVER_size_t len, __CPROVER_size_t s)\n"
  "{\n"
  "}                        \n"
  "\n"
},
{ "c::strcpy",
  "#line 1 \"<builtin-library>-strcpy\"\n"
  "\n"
  "#ifndef __CPROVER_STRING_H_INCLUDED\n"
  "#include <string.h>\n"
  "#define __CPROVER_STRING_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "#undef strcpy\n"
  "\n"
  "inline char *strcpy(char *dst, const char *src)\n"
  "{\n"
  "  __CPROVER_HIDE:;\n"
  "  #ifdef __CPROVER_STRING_ABSTRACTION\n"
  "  __CPROVER_assert(__CPROVER_is_zero_string(src), \"strcpy zero-termination of 2nd argument\");\n"
  "  __CPROVER_assert(__CPROVER_buffer_size(dst)>__CPROVER_zero_string_length(src), \"strcpy buffer overflow\");\n"
  "  dst[__CPROVER_zero_string_length(src)]=0;\n"
  "  __CPROVER_is_zero_string(dst)=1;\n"
  "  __CPROVER_zero_string_length(dst)=__CPROVER_zero_string_length(src);\n"
  "  #else\n"
  "  __CPROVER_size_t i=0;\n"
  "  char ch;\n"
  "  do\n"
  "  {\n"
  "    ch=src[i];\n"
  "    dst[i]=ch;\n"
  "    i++;\n"
  "  }\n"
  "  while(ch!=(char)0);\n"
  "  #endif\n"
  "  return dst;\n"
  "}\n"
  "\n"
},
{ "c::strncpy",
  "#line 1 \"<builtin-library>-strncpy\"\n"
  "\n"
  "#ifndef __CPROVER_STRING_H_INCLUDED\n"
  "#include <string.h>\n"
  "#define __CPROVER_STRING_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "#undef strncpy\n"
  "\n"
  "inline char *strncpy(char *dst, const char *src, size_t n)\n"
  "{\n"
  "  __CPROVER_HIDE:;\n"
  "  #ifdef __CPROVER_STRING_ABSTRACTION\n"
  "  __CPROVER_assert(__CPROVER_is_zero_string(src), \"strncpy zero-termination of 2nd argument\");\n"
  "  __CPROVER_assert(__CPROVER_buffer_size(dst)>=n, \"strncpy buffer overflow\");\n"
  "  __CPROVER_is_zero_string(dst)=__CPROVER_zero_string_length(src)<n;\n"
  "  __CPROVER_zero_string_length(dst)=__CPROVER_zero_string_length(src);  \n"
  "  #else\n"
  "  __CPROVER_size_t i=0;\n"
  "  char ch;\n"
  "\n"
  "  for( ; i<n && (ch=src[i])!=(char)0; i++)\n"
  "    dst[i]=ch;\n"
  "\n"
  "  for( ; i<n ; i++)\n"
  "    dst[i]=0;\n"
  "  #endif\n"
  "  return dst;\n"
  "}\n"
  "\n"
},
{ "c::strcat",
  "#line 1 \"<builtin-library>-strcat\"\n"
  "\n"
  "#ifndef __CPROVER_STRING_H_INCLUDED\n"
  "#include <string.h>\n"
  "#define __CPROVER_STRING_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "#undef strcat\n"
  "\n"
  "inline char *strcat(char *dst, const char *src)\n"
  "{\n"
  "  __CPROVER_HIDE:;\n"
  "  #ifdef __CPROVER_STRING_ABSTRACTION\n"
  "  __CPROVER_size_t new_size;\n"
  "  __CPROVER_assert(__CPROVER_is_zero_string(dst), \"strcat zero-termination of 1st argument\");\n"
  "  __CPROVER_assert(__CPROVER_is_zero_string(src), \"strcat zero-termination of 2nd argument\");\n"
  "  new_size=__CPROVER_zero_string_length(dst)+__CPROVER_zero_string_length(src);\n"
  "  __CPROVER_assert(__CPROVER_buffer_size(dst)>new_size,\n"
  "                   \"strcat buffer overflow\");\n"
  "  __CPROVER_size_t old_size=__CPROVER_zero_string_length(dst);\n"
  "  //\"  for(size_t i=0; i<__CPROVER_zero_string_length(src); i++)\n"
  "  //\"    dst[old_size+i];\n"
  "  dst[new_size]=0;\n"
  "  __CPROVER_is_zero_string(dst)=1;\n"
  "  __CPROVER_zero_string_length(dst)=new_size;\n"
  "  #else\n"
  "  __CPROVER_size_t i=0;\n"
  "  while(dst[i]!=0) i++;\n"
  "\n"
  "  __CPROVER_size_t j=0;\n"
  "  char ch;\n"
  "  do\n"
  "  {\n"
  "    char ch=src[j];\n"
  "    dst[i]=ch;\n"
  "    i++;\n"
  "    j++;\n"
  "  }\n"
  "  while(ch!=(char)0);\n"
  "  #endif\n"
  "  return dst;\n"
  "}\n"
  "\n"
},
{ "c::strncat",
  "#line 1 \"<builtin-library>-strncat\"\n"
  "\n"
  "#ifndef __CPROVER_STRING_H_INCLUDED\n"
  "#include <string.h>\n"
  "#define __CPROVER_STRING_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "#undef strncat\n"
  "\n"
  "inline char *strncat(char *dst, const char *src, size_t n)\n"
  "{\n"
  "  __CPROVER_HIDE:;\n"
  "  #ifdef __CPROVER_STRING_ABSTRACTION\n"
  "  __CPROVER_size_t additional, new_size;\n"
  "  __CPROVER_assert(__CPROVER_is_zero_string(dst), \"strncat zero-termination of 1st argument\");\n"
  "  __CPROVER_assert(__CPROVER_is_zero_string(src) || __CPROVER_buffer_size(src)>=n, \"strncat zero-termination of 2nd argument\");\n"
  "  additional=(n<__CPROVER_zero_string_length(src))?n:__CPROVER_zero_string_length(src);\n"
  "  new_size=__CPROVER_is_zero_string(dst)+additional; \n"
  "  __CPROVER_assert(__CPROVER_buffer_size(dst)>new_size,\n"
  "                   \"strncat buffer overflow\");\n"
  "  __CPROVER_size_t dest_len=__CPROVER_zero_string_length(dst); \n"
  "  __CPROVER_size_t i;\n"
  "  for (i = 0 ; i < n && i<__CPROVER_zero_string_length(src) ; i++)\n"
  "    dst[dest_len + i] = src[i];\n"
  "  dst[dest_len + i] = 0;\n"
  "  __CPROVER_is_zero_string(dst)=1;\n"
  "  __CPROVER_zero_string_length(dst)=new_size;\n"
  "  #else\n"
  "  #endif\n"
  "  return dst;\n"
  "}\n"
  "\n"
},
{ "c::strcmp",
  "#line 1 \"<builtin-library>-strcmp\"\n"
  "\n"
  "#ifndef __CPROVER_STRING_H_INCLUDED\n"
  "#include <string.h>\n"
  "#define __CPROVER_STRING_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "#undef strcmp\n"
  "\n"
  "inline int strcmp(const char *s1, const char *s2)\n"
  "{\n"
  "  __CPROVER_HIDE:;\n"
  "  int retval;\n"
  "  if(s1!=0 && s1==s2) return 0;\n"
  "  #ifdef __CPROVER_STRING_ABSTRACTION\n"
  "  __CPROVER_assert(__CPROVER_is_zero_string(s1), \"strcmp zero-termination of 1st argument\");\n"
  "  __CPROVER_assert(__CPROVER_is_zero_string(s2), \"strcmp zero-termination of 2nd argument\");\n"
  "  if(__CPROVER_zero_string_length(s1) != __CPROVER_zero_string_length(s2)) __CPROVER_assume(retval!=0);\n"
  "  return retval;\n"
  "  #else\n"
  "  __CPROVER_size_t i=0;\n"
  "  unsigned char ch1, ch2;\n"
  "  do\n"
  "  {\n"
  "    ch1=s1[i];\n"
  "    ch2=s2[i];\n"
  "\n"
  "    if(ch1==ch2)\n"
  "    {\n"
  "    }\n"
  "    else if(ch1<ch2)\n"
  "      return -1;\n"
  "    else\n"
  "      return 1;\n"
  "\n"
  "    i++;\n"
  "  }\n"
  "  while(ch1!=0 && ch2!=0);\n"
  "  return 0;\n"
  "  #endif\n"
  "}\n"
  "\n"
},
{ "c::strcasecmp",
  "#line 1 \"<builtin-library>-strcasecmp\"\n"
  "\n"
  "#ifndef __CPROVER_STRING_H_INCLUDED\n"
  "#include <string.h>\n"
  "#define __CPROVER_STRING_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "#undef strcasecmp\n"
  "\n"
  "inline int strcasecmp(const char *s1, const char *s2)\n"
  "{\n"
  "  __CPROVER_HIDE:;\n"
  "  int retval;\n"
  "  if(s1!=0 && s1==s2) return 0;\n"
  "  #ifdef __CPROVER_STRING_ABSTRACTION\n"
  "  __CPROVER_assert(__CPROVER_is_zero_string(s1), \"strcasecmp zero-termination of 1st argument\");\n"
  "  __CPROVER_assert(__CPROVER_is_zero_string(s2), \"strcasecmp zero-termination of 2nd argument\");\n"
  "  if(__CPROVER_zero_string_length(s1) != __CPROVER_zero_string_length(s2)) __CPROVER_assume(retval!=0);\n"
  "  return retval;\n"
  "  #else\n"
  "  __CPROVER_size_t i=0;\n"
  "  unsigned char ch1, ch2;\n"
  "  do\n"
  "  {\n"
  "    ch1=s1[i];\n"
  "    ch2=s2[i];\n"
  "    \n"
  "    if(ch1>='A' && ch1<='Z') ch1+=('a'-'A');\n"
  "    if(ch2>='A' && ch2<='Z') ch2+=('a'-'A');\n"
  "\n"
  "    if(ch1==ch2)\n"
  "    {\n"
  "    }\n"
  "    else if(ch1<ch2)\n"
  "      return -1;\n"
  "    else\n"
  "      return 1;\n"
  "\n"
  "    i++;\n"
  "  }\n"
  "  while(ch1!=0 && ch2!=0);\n"
  "  return 0;\n"
  "  #endif\n"
  "}\n"
  "\n"
},
{ "c::strncmp",
  "#line 1 \"<builtin-library>-strncmp\"\n"
  "\n"
  "#ifndef __CPROVER_STRING_H_INCLUDED\n"
  "#include <string.h>\n"
  "#define __CPROVER_STRING_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "#undef strncmp\n"
  "\n"
  "inline int strncmp(const char *s1, const char *s2, size_t n)\n"
  "{\n"
  "  __CPROVER_HIDE:;\n"
  "  if(s1!=0 && s1==s2) return 0;\n"
  "  #ifdef __CPROVER_STRING_ABSTRACTION\n"
  "  __CPROVER_assert(__CPROVER_is_zero_string(s1) || __CPROVER_buffer_size(s1)>=n, \"strncmp zero-termination of 1st argument\");\n"
  "  __CPROVER_assert(__CPROVER_is_zero_string(s2) || __CPROVER_buffer_size(s2)>=n, \"strncmp zero-termination of 2nd argument\");\n"
  "  #else\n"
  "  __CPROVER_size_t i=0;\n"
  "  unsigned char ch1, ch2;\n"
  "  do\n"
  "  {\n"
  "    ch1=s1[i];\n"
  "    ch2=s2[i];\n"
  "\n"
  "    if(ch1==ch2)\n"
  "    {\n"
  "    }\n"
  "    else if(ch1<ch2)\n"
  "      return -1;\n"
  "    else\n"
  "      return 1;\n"
  "\n"
  "    i++;\n"
  "  }\n"
  "  while(ch1!=0 && ch2!=0 && i<n);\n"
  "  return 0;\n"
  "  #endif\n"
  "}\n"
  "\n"
},
{ "c::strncasecmp",
  "#line 1 \"<builtin-library>-strncasecmp\"\n"
  "\n"
  "#ifndef __CPROVER_STRING_H_INCLUDED\n"
  "#include <string.h>\n"
  "#define __CPROVER_STRING_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "#undef strncasecmp\n"
  "\n"
  "inline int strncasecmp(const char *s1, const char *s2, size_t n)\n"
  "{\n"
  "  __CPROVER_HIDE:;\n"
  "  int retval;\n"
  "  if(s1!=0 && s1==s2) return 0;\n"
  "  #ifdef __CPROVER_STRING_ABSTRACTION\n"
  "  __CPROVER_assert(__CPROVER_is_zero_string(s1), \"strncasecmp zero-termination of 1st argument\");\n"
  "  __CPROVER_assert(__CPROVER_is_zero_string(s2), \"strncasecmp zero-termination of 2nd argument\");\n"
  "  return retval;\n"
  "  #else\n"
  "  __CPROVER_size_t i=0;\n"
  "  unsigned char ch1, ch2;\n"
  "  do\n"
  "  {\n"
  "    ch1=s1[i];\n"
  "    ch2=s2[i];\n"
  "    \n"
  "    if(ch1>='A' && ch1<='Z') ch1+=('a'-'A');\n"
  "    if(ch2>='A' && ch2<='Z') ch2+=('a'-'A');\n"
  "\n"
  "    if(ch1==ch2)\n"
  "    {\n"
  "    }\n"
  "    else if(ch1<ch2)\n"
  "      return -1;\n"
  "    else\n"
  "      return 1;\n"
  "\n"
  "    i++;\n"
  "  }\n"
  "  while(ch1!=0 && ch2!=0 && i<n);\n"
  "  return 0;\n"
  "  #endif\n"
  "}\n"
  "\n"
},
{ "c::strlen",
  "#line 1 \"<builtin-library>-strlen\"\n"
  "\n"
  "#ifndef __CPROVER_STRING_H_INCLUDED\n"
  "#include <string.h>\n"
  "#define __CPROVER_STRING_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "#undef strlen\n"
  "\n"
  "inline size_t strlen(const char *s)\n"
  "{\n"
  "  __CPROVER_HIDE:;\n"
  "  #ifdef __CPROVER_STRING_ABSTRACTION\n"
  "  __CPROVER_assert(__CPROVER_is_zero_string(s), \"strlen zero-termination\");\n"
  "  return __CPROVER_zero_string_length(s);\n"
  "  #else\n"
  "  __CPROVER_size_t len=0;\n"
  "  while(s[len]!=0) len++;\n"
  "  return len;\n"
  "  #endif\n"
  "}\n"
  "\n"
},
{ "c::strdup",
  "#line 1 \"<builtin-library>-strdup\"\n"
  "\n"
  "#ifndef __CPROVER_STRING_H_INCLUDED\n"
  "#include <string.h>\n"
  "#define __CPROVER_STRING_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "#ifndef __CPROVER_STDLIB_H_INCLUDED\n"
  "#include <stdlib.h>\n"
  "#define __CPROVER_STDLIB_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "#undef strdup\n"
  "#undef strcpy\n"
  "\n"
  "inline char *strdup(const char *str)\n"
  "{\n"
  "  __CPROVER_HIDE:;\n"
  "  __CPROVER_size_t bufsz;\n"
  "  bufsz=(strlen(str)+1);\n"
  "  char *cpy=(char *)malloc(bufsz*sizeof(char));\n"
  "  if(cpy==((void *)0)) return 0;\n"
  "  #ifdef __CPROVER_STRING_ABSTRACTION\n"
  "  __CPROVER_assume(__CPROVER_buffer_size(cpy)==bufsz);\n"
  "  #endif\n"
  "  strcpy(cpy, str);\n"
  "  return cpy;\n"
  "}\n"
  "\n"
},
{ "c::memcpy",
  "#line 1 \"<builtin-library>-memcpy\"\n"
  "\n"
  "#ifndef __CPROVER_STRING_H_INCLUDED\n"
  "#include <string.h>\n"
  "#define __CPROVER_STRING_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "#undef memcpy\n"
  "\n"
  "inline void *memcpy(void *dst, const void *src, size_t n)\n"
  "{\n"
  "  __CPROVER_HIDE:\n"
  "  #ifdef __CPROVER_STRING_ABSTRACTION\n"
  "  __CPROVER_assert(__CPROVER_buffer_size(src)>=n, \"memcpy buffer overflow\");\n"
  "  __CPROVER_assert(__CPROVER_buffer_size(dst)>=n, \"memcpy buffer overflow\");\n"
  "  //  for(size_t i=0; i<n ; i++) dst[i]=src[i];\n"
  "  if(__CPROVER_is_zero_string(src) &&\n"
  "     n > __CPROVER_zero_string_length(src))\n"
  "  {\n"
  "    __CPROVER_is_zero_string(dst)=1;\n"
  "    __CPROVER_zero_string_length(dst)=__CPROVER_zero_string_length(src);\n"
  "  }\n"
  "  else if(!(__CPROVER_is_zero_string(dst) &&\n"
  "            n <= __CPROVER_zero_string_length(dst)))\n"
  "    __CPROVER_is_zero_string(dst)=0;\n"
  "  #else\n"
  "  for(__CPROVER_size_t i=0; i<n ; i++) ((char *)dst)[i]=((const char *)src)[i];\n"
  "  #endif\n"
  "  return dst;\n"
  "}\n"
  "\n"
},
{ "c::memset",
  "#line 1 \"<builtin-library>-memset\"\n"
  "\n"
  "#ifndef __CPROVER_STRING_H_INCLUDED\n"
  "#include <string.h>\n"
  "#define __CPROVER_STRING_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "#undef memset\n"
  "\n"
  "inline void *memset(void *s, int c, size_t n)\n"
  "{\n"
  "  __CPROVER_HIDE:\n"
  "  #ifdef __CPROVER_STRING_ABSTRACTION\n"
  "  __CPROVER_assert(__CPROVER_buffer_size(s)>=n, \"memset buffer overflow\");\n"
  "  //  for(size_t i=0; i<n ; i++) s[i]=c;\n"
  "  if(__CPROVER_is_zero_string(s) &&\n"
  "     n > __CPROVER_zero_string_length(s))\n"
  "  {\n"
  "    __CPROVER_is_zero_string(s)=1;\n"
  "  }\n"
  "  else if(c==0)\n"
  "  {\n"
  "    __CPROVER_is_zero_string(s)=1;\n"
  "    __CPROVER_zero_string_length(s)=0;\n"
  "  }\n"
  "  else\n"
  "    __CPROVER_is_zero_string(s)=0;\n"
  "  #else\n"
  "  char *sp=s;\n"
  "  for(__CPROVER_size_t i=0; i<n ; i++) sp[i]=c;\n"
  "  #endif\n"
  "  return s;\n"
  "}\n"
  "\n"
},
{ "c::memmove",
  "#line 1 \"<builtin-library>-memmove\"\n"
  "\n"
  "#ifndef __CPROVER_STRING_H_INCLUDED\n"
  "#include <string.h>\n"
  "#define __CPROVER_STRING_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "#undef memmove\n"
  "\n"
  "inline void *memmove(void *dest, const void *src, size_t n)\n"
  "{\n"
  "  __CPROVER_HIDE:\n"
  "  #ifdef __CPROVER_STRING_ABSTRACTION\n"
  "  __CPROVER_assert(__CPROVER_buffer_size(src)>=n, \"memmove buffer overflow\");\n"
  "  // dst = src (with overlap allowed)\n"
  "  if(__CPROVER_is_zero_string(src) &&\n"
  "     n > __CPROVER_zero_string_length(src))\n"
  "  {\n"
  "    __CPROVER_is_zero_string(src)=1;\n"
  "    __CPROVER_zero_string_length(dest)=__CPROVER_zero_string_length(src);\n"
  "  }\n"
  "  else\n"
  "    __CPROVER_is_zero_string(dest)=0;\n"
  "  #else\n"
  "  if(dest-src>=n)\n"
  "  {\n"
  "    for(__CPROVER_size_t i=0; i<n; i++) ((char *)dest)[i]=((const char *)src)[i];\n"
  "  }\n"
  "  else \n"
  "  {\n"
  "    for(__CPROVER_size_t i=n; i>0; i--) ((char *)dest)[i-1]=((const char *)src)[i-1];\n"
  "  }\n"
  "  #endif\n"
  "  return dest;\n"
  "}\n"
  "\n"
},
{ "c::memcmp",
  "#line 1 \"<builtin-library>-memcmp\"\n"
  "\n"
  "#ifndef __CPROVER_STRING_H_INCLUDED\n"
  "#include <string.h>\n"
  "#define __CPROVER_STRING_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "#undef memcmp\n"
  "\n"
  "inline int memcmp(const void *s1, const void *s2, size_t n)\n"
  "{\n"
  "  __CPROVER_HIDE:;\n"
  "  int res;\n"
  "  #ifdef __CPROVER_STRING_ABSTRACTION\n"
  "  __CPROVER_assert(__CPROVER_buffer_size(s1)>=n, \"memcmp buffer overflow of 1st argument\");\n"
  "  __CPROVER_assert(__CPROVER_buffer_size(s2)>=n, \"memcmp buffer overflow of 2nd argument\");\n"
  "  #else\n"
  "  const unsigned char *sc1=s1, *sc2=s2;\n"
  "  for(; n!=0; n--)\n"
  "  {\n"
  "    res = (s1++) - (s2++);\n"
  "    if (res != 0)\n"
  "      return res;\n"
  "  }\n"
  "  #endif\n"
  "  return res;\n"
  "}\n"
  "\n"
},
{ "c::strchr",
  "#line 1 \"<builtin-library>-strchr\"\n"
  "\n"
  "#ifndef __CPROVER_STRING_H_INCLUDED\n"
  "#include <string.h>\n"
  "#define __CPROVER_STRING_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "#undef strchr\n"
  "\n"
  "inline char *strchr(const char *src, int c)\n"
  "{\n"
  "  __CPROVER_HIDE:;\n"
  "  #ifdef __CPROVER_STRING_ABSTRACTION\n"
  "  __CPROVER_assert(__CPROVER_is_zero_string(src), \"strchr zero-termination of string argument\");\n"
  "  _Bool found;\n"
  "  __CPROVER_size_t i;\n"
  "  return found?src+i:0;\n"
  "  #else\n"
  "  for(__CPROVER_size_t i=0; src[i]!=0; i++)\n"
  "    if(src[i]==(char)c)\n"
  "      return ((char *)src)+i; // cast away const-ness\n"
  "\n"
  "  return 0;\n"
  "  #endif\n"
  "}\n"
  "\n"
},
{ "c::strrchr",
  "#line 1 \"<builtin-library>-strrchr\"\n"
  "\n"
  "#ifndef __CPROVER_STRING_H_INCLUDED\n"
  "#include <string.h>\n"
  "#define __CPROVER_STRING_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "#undef strchr\n"
  "\n"
  "inline char *strrchr(const char *src, int c)\n"
  "{\n"
  "  __CPROVER_HIDE:;\n"
  "  #ifdef __CPROVER_STRING_ABSTRACTION\n"
  "  __CPROVER_assert(__CPROVER_is_zero_string(src), \"strrchr zero-termination of string argument\");\n"
  "  _Bool found;\n"
  "  __CPROVER_size_t i;\n"
  "  return found?((char *)src)+i:0;\n"
  "  #else\n"
  "  char *res=0;\n"
  "  for(__CPROVER_size_t i=0; src[i]!=0; i++)\n"
  "    if(src[i]==(char)c) res=((char *)src)+i;\n"
  "  return res;\n"
  "  #endif\n"
  "}\n"
  "\n"
},
{ "c::openlog",
  "#line 1 \"<builtin-library>-openlog\"\n"
  "\n"
  "#ifndef __CPROVER_SYSLOG_H_INCLUDED\n"
  "#include <syslog.h>\n"
  "#define __CPROVER_SYSLOG_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "void openlog(const char *ident, int option, int facility)\n"
  "{\n"
  "}\n"
  "\n"
},
{ "c::closelog",
  "#line 1 \"<builtin-library>-closelog\"\n"
  "\n"
  "#ifndef __CPROVER_SYSLOG_H_INCLUDED\n"
  "#include <syslog.h>\n"
  "#define __CPROVER_SYSLOG_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "void closelog(void)\n"
  "{\n"
  "}\n"
  "\n"
},
{ "c::syslog",
  "#line 1 \"<builtin-library>-syslog\"\n"
  "\n"
  "#ifndef __CPROVER_SYSLOG_H_INCLUDED\n"
  "#include <syslog.h>\n"
  "#define __CPROVER_SYSLOG_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "void syslog(int priority, const char *format, ...)\n"
  "{\n"
  "  // should check arguments\n"
  "}\n"
},
{ "c::time",
  "#line 1 \"<builtin-library>-time\"\n"
  "\n"
  "#ifndef __CPROVER_TIME_H_INCLUDED\n"
  "#include <time.h>\n"
  "#define __CPROVER_TIME_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "#undef time\n"
  "\n"
  "time_t time(time_t *tloc)\n"
  "{\n"
  "  time_t res;\n"
  "  if(!tloc) *tloc=res;\n"
  "  return res;\n"
  "}\n"
  "\n"
},
{ "c::gmtime",
  "#line 1 \"<builtin-library>-gmtime\"\n"
  "\n"
  "#ifndef __CPROVER_TIME_H_INCLUDED\n"
  "#include <time.h>\n"
  "#define __CPROVER_TIME_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "#undef gmtime\n"
  "\n"
  "struct tm *gmtime(const time_t *clock)\n"
  "{\n"
  "  // not very general, may be too restrictive\n"
  "  // need to set the fields to something meaningful\n"
  "  *clock;\n"
  "  static struct tm return_value;\n"
  "  return &return_value;\n"
  "}\n"
  "\n"
},
{ "c::gmtime_r",
  "#line 1 \"<builtin-library>-gmtime_r\"\n"
  "\n"
  "#ifndef __CPROVER_TIME_H_INCLUDED\n"
  "#include <time.h>\n"
  "#define __CPROVER_TIME_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "#undef gmtime\n"
  "\n"
  "struct tm *gmtime_r(const time_t *clock, struct tm *result)\n"
  "{\n"
  "  // need to set the fields to something meaningful\n"
  "  *clock;\n"
  "  return result;\n"
  "}\n"
  "\n"
},
{ "c::localtime",
  "#line 1 \"<builtin-library>-localtime\"\n"
  "\n"
  "#ifndef __CPROVER_TIME_H_INCLUDED\n"
  "#include <time.h>\n"
  "#define __CPROVER_TIME_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "#undef localtime\n"
  "\n"
  "struct tm *localtime(const time_t *clock)\n"
  "{\n"
  "  // not very general, may be too restrictive\n"
  "  // need to set the fields to something meaningful\n"
  "  *clock;\n"
  "  static struct tm return_value;\n"
  "  return &return_value;\n"
  "}\n"
  "\n"
},
{ "c::localtime_r",
  "#line 1 \"<builtin-library>-localtime_r\"\n"
  "\n"
  "#ifndef __CPROVER_TIME_H_INCLUDED\n"
  "#include <time.h>\n"
  "#define __CPROVER_TIME_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "#undef localtime\n"
  "\n"
  "struct tm *localtime_r(const time_t *clock, struct tm *result)\n"
  "{\n"
  "  // need to set the fields to something meaningful\n"
  "  *clock;\n"
  "  return result;\n"
  "}\n"
  "\n"
},
{ "c::mktime",
  "#line 1 \"<builtin-library>-mktime\"\n"
  "\n"
  "#ifndef __CPROVER_TIME_H_INCLUDED\n"
  "#include <time.h>\n"
  "#define __CPROVER_TIME_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "#undef mktime\n"
  "\n"
  "time_t mktime(struct tm *timeptr)\n"
  "{\n"
  "  *timeptr;\n"
  "  time_t result;\n"
  "  return result;\n"
  "}\n"
  "\n"
},
{ "c::timegm",
  "#line 1 \"<builtin-library>-timegm\"\n"
  "\n"
  "#ifndef __CPROVER_TIME_H_INCLUDED\n"
  "#include <time.h>\n"
  "#define __CPROVER_TIME_H_INCLUDED\n"
  "#endif\n"
  "\n"
  "#undef timegm\n"
  "\n"
  "time_t timegm(struct tm *timeptr)\n"
  "{\n"
  "  *timeptr;\n"
  "  time_t result;\n"
  "  return result;\n"
  "}\n"
  "\n"
},
{ "c::sleep",
  "#line 1 \"<builtin-library>-sleep\"\n"
  "\n"
  "unsigned nondet_uint();\n"
  "\n"
  "unsigned int sleep(unsigned int seconds)\n"
  "{\n"
  "  // do nothing, but return nondet value\n"
  "  unsigned remaining_time=nondet_uint();\n"
  "  \n"
  "  if(remaining_time>seconds) remaining_time=seconds;\n"
  "  \n"
  "  return remaining_time;\n"
  "}\n"
  "\n"
},
{ "c::unlink",
  "#line 1 \"<builtin-library>-unlink\"\n"
  "\n"
  "void unlink(const char *s)\n"
  "{\n"
  "  __CPROVER_hide:;\n"
  "  #ifdef __CPROVER_STRING_ABSTRACTION\n"
  "  __CPROVER_assert(__CPROVER_is_zero_string(s), \"unlink zero-termination\");\n"
  "  #endif\n"
  "}\n"
  "\n"
},
{ "c::QueryPerformanceFrequency",
  "#line 1 \"<builtin-library>-QueryPerformanceFrequency\"\n"
  "\n"
  "#include <windows.h>\n"
  "\n"
  "BOOL QueryPerformanceFrequency(LARGE_INTEGER *lpFrequency)\n"
  "{\n"
  "  __CPROVER_HIDE:;\n"
  "  __int64 result;\n"
  "  lpFrequency->QuadPart=result;\n"
  "  _Bool error;\n"
  "  if(error) return 0;\n"
  "  __CPROVER_assume(result!=0);\n"
  "  return 1;\n"
  "}\n"
  "\n"
},
{ "c::ExitThread",
  "#line 1 \"<builtin-library>-ExitThread\"\n"
  "\n"
  "#include <windows.h>\n"
  "\n"
  "VOID ExitThread(DWORD dwExitCode)\n"
  "{\n"
  "  // never returns\n"
  "  __CPROVER_assume(0);\n"
  "}\n"
  "\n"
},
{ "c::CreateThread",
  "#line 1 \"<builtin-library>-CreateThread\"\n"
  "\n"
  "#include <windows.h>\n"
  "\n"
  "HANDLE CreateThread(\n"
  "  LPSECURITY_ATTRIBUTES lpThreadAttributes,\n"
  "  SIZE_T dwStackSize,\n"
  "  LPTHREAD_START_ROUTINE lpStartAddress,\n"
  "  LPVOID lpParameter,\n"
  "  DWORD dwCreationFlags,\n"
  "  LPDWORD lpThreadId\n"
  ")\n"
  "{\n"
  "  __CPROVER_HIDE:;\n"
  "  DWORD thread_id;\n"
  "\n"
  "  if(lpThreadId) *lpThreadId=thread_id;\n"
  "  __CPROVER_ASYNC_1: lpStartAddress(lpParameter);\n"
  "  \n"
  "  HANDLE handle;\n"
  "  return handle;\n"
  "}\n"
},
{ 0, 0 }
};
